Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	fst(0,Z)	→ nil
2:	fst(s(X),cons(Y,Z))	→ cons(Y,n__fst(activate(X),activate(Z)))
3:	from(X)	→ cons(X,n__from(s(X)))
4:	add(0,X)	→ X
5:	add(s(X),Y)	→ s(n__add(activate(X),Y))
6:	len(nil)	→ 0
7:	len(cons(X,Z))	→ s(n__len(activate(Z)))
8:	fst(X1,X2)	→ n__fst(X1,X2)
9:	from(X)	→ n__from(X)
10:	add(X1,X2)	→ n__add(X1,X2)
11:	len(X)	→ n__len(X)
12:	activate(n__fst(X1,X2))	→ fst(X1,X2)
13:	activate(n__from(X))	→ from(X)
14:	activate(n__add(X1,X2))	→ add(X1,X2)
15:	activate(n__len(X))	→ len(X)
16:	activate(X)	→ X

There are 8 dependency pairs:

The approximated dependency graph contains one SCC: {17-21,23,24}.

Consider the SCC {17-21,23,24}. There are no usable rules. By taking the AF π with π(ACTIVATE) = π(ADD) = π(LEN) = π(n__add) = π(n__len) = π(s) = 1 and π(cons) = 2 together with the lexicographic path order with precedence n__fst ≻ FST, the rules in {19,20,23,24} are weakly decreasing and the rules in {17,18,21} are strictly decreasing. There is one new SCC.
- Consider the SCC {19,20,23,24}. By taking the AF π with π(ACTIVATE) = π(ADD) = π(LEN) = π(n__add) = π(n__len) = π(s) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, the rules in {19,23,24} are weakly decreasing and rule 20 is strictly decreasing. There is one new SCC.
  - Consider the SCC {19,23}. By taking the AF π with π(ACTIVATE) = π(ADD) = π(n__add) = 1 together with the lexicographic path order with empty precedence, rule 23 is weakly decreasing and rule 19 is strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.05 seconds) --- May 4, 2006